Inference at * 1 0 1 3 
Iof proof for Lemma nat ind:

.....upcase..... NILNIL

1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. j : 
5. 0 < j
6. ((j - 1)  0 )  P(j - 1)
  (j  0 )  P(j) 

latex

 by D 0 

latex

 1: 

 1: 7. j  0 
 1:   P(j)
 2: .....wf..... NILNIL

 2:   (j  0 )  
 .

Definitions	Type, s = t, a < b, , n - m, , x:A. B(x), #$n, , f(a), x:AB(x), i  j , P  Q, x(s), t  T,
Lemmas	ge wf